logical implication

n : a logical relation between propositions p and q of the form

`if p then q'; if p is true then q cannot be false [syn:

{implication}, {conditional relation}]

logical relation

A {relation} R satisfying

f R g <◦> For all a, b, a R b ◦> f a R g b

This definition, by Plotkin, can be used to extend the

definition of a relation on the types of a and b to a relation

on functions.